Issue3323q.agda:10,12-13
Unexpected modality/relevance annotation in b
when checking the definition of T
